| Definitions | t  T,  x:A. B(x), P   Q, d-world-state(D;i), {x:A| B(x) },  , {i..j }, Type, d-comp(D;v;sched;dec), Dsys, destination(l), M.din(l,tg), source(l), M.dout2(l;tg), IdLnk, Unit, left+right, locl(a), M.da(a), #$n, n-m, f(a), 1of(t), M(i), M.init(x)?v,  x.A(x), i= j, if b t else f fi, M.state, Id, x:A  B(x), s = t,  , Prop,  b,  A, b,  , x:A B(x), P & Q, P  Q, M.ds(x), State(ds), False, A B, Top, f(x)?z, s ~ t, a<b, i j < k, -n, n+m, Void, hd(l), let x = a in b(x), d-partial-world(D;f;t';s), World, Knd, x,y. t(x;y), x. t(x), null, outl(x), inr(x), doact(k;v), isl(x), queue(l;t), mval(m), mtag(m), rcv(l,tg), ||as||, i<j, i = j, p  q, Case b of inl(x) s(x) ; inr(y) t(y), a = b, kindcase(k; a.f(a); l,t.g(l;t) ), Action(dec), tag(k), lnk(k), act(k), islocal(k), Msg, ij, P  Q, p q, True,  T, P Q, 2of(t), outr(x), i j, Msg(M), {T}, SQType(T), mlnk(m), <a,b>, MsgA, w.M, M.sends(k,s,v), filter(P;l), nil, type List, M.Msg, Msg(da), M.ef(k,x,s,v)?w, d-decl(D;i), S  T, w-action-dec(TA;M;i), M.dout(l,tg), inl(x) |
| Lemmas | nat properties, d-decl wf, subtype rel self, ma-ef-val wf, subtype rel list, filter type, mlnk wf d, ma-send-val wf, ma-msg wf, Msg wf, mlnk wf, null-action wf, assert-d-eq-Loc, msga wf, mlnk-hd-w-queue, assert-eq-id, hd wf, pi1 wf, pi2 wf, doact wf, rcv wf, assert of band, and functionality wrt iff, assert of lt int, bnot thru band, squash wf, true wf, bnot of lt int, assert of bor, or functionality wrt iff, assert of le int, band wf, lt int wf, bor wf, le int wf, d-eq-Loc wf, length wf1, w-Msg wf, w-queue wf, action wf, kindcase wf, ifthenelse wf, eq id wf, Knd wf, d-partial-world wf, world wf, le wf, ma-ds wf, ma-init-val wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, ma-da wf, locl wf, unit wf, IdLnk wf, ma-dout2 wf, lsrc wf, ma-din wf, ldst wf, dsys wf, nat wf, int seg wf, d-world-state wf, Id wf, ma-st wf, d-m wf |
M(destination(l)).din(l,tg))
